Nuprl Definition : d-sub
0,22
postcript
pdf
D1
D2
==
i
:Id. M(
i
)
M(
i
)
latex
clarification:
d-sub{i:l}(
D1
;
D2
) ==
i
:Id. ma-sub{i:l}(d-m(
D1
;
i
); d-m(
D2
;
i
))
latex
Definitions
M(
i
)
,
M1
M2
,
Id
,
x
:
A
.
B
(
x
)
,
D1
D2
FDL editor aliases
d-sub
origin
D2 == 
i:Id. M(i) M(i)
i:Id. ma-sub{i:l}(d-m(D1; i); d-m(D2; i)) D2 == i:Id. M(i) M(i)
i:Id. ma-sub{i:l}(d-m(D1; i); d-m(D2; i)) M2x:A. B(x) D2